(declare-const A (Seq Int))
(declare-const m Int)
(assert (<= 0 m))
(assert (< m (seq.len A)))
(assert (forall ((i Int)) (<= (seq.nth A i) (seq.nth A m))))
(declare-const f_A (Seq Int))
(assert (= f_A (let ((max (seq.nth A m))(n (seq.len A))) (ite (or (>= max n) (< max 0)) (seq.unit 74) (seq.++ (seq.extract A 0 m) (seq.extract A (+ m 1) (- (- n 1) m)))))))
(assert (and (spec f_A) (not (spec A))))
(declare-const spec_f_A Bool)
(assert (= (spec f_A) spec_f_A))
(assert (< 2 (seq.len A)))
(assert (< (seq.len A) 5))
(check-sat)
